$\forall$$w$:World, $e$:E.
\\[0ex]($\neg$($\uparrow$first($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$t$:$\mathbb{N}$. ((time(pred($e$))+1) $\leq$ $t$) $\Rightarrow$ ($t$ $<$ time($e$)) $\Rightarrow$ ($\uparrow$isnull(a(loc($e$);$t$))))